Propositions as Types

Propositions as Types(型としての命題)

数理論理学での論理は、依存型理論での型と本質的に同じと見なすことができるというやつ

命題(proposision) = 型(type)

$ \mathrm{ proof : Proposition} \cong \mathrm{term : Type}

証明を関数(λ項: 証明項と呼ぶ)、命題を証明項のデータ型とみなす

$ \begin{array}{c|c} \mathrm{英語} & \mathrm{型理論} \\ \hline \mathrm{True} & \mathbf{1} \\ \mathrm{False} & \mathbf{0} \\ \text{A and B} & A \times B \\ \text{A or B} & A + B \\ \text{If A then B} & A \rightarrow B \\ \text{A if and only if B} & (A \rightarrow B ) \times (B \rightarrow A) \\ \text{Not A} & A \rightarrow \mathbf{0} \end{array}

$ \begin{array}{c|c} \mathrm{論理} & \mathrm{型理論} \\ \hline \mathrm{True} & \mathbf{1} \\ \mathrm{False} & \mathbf{0} \\ A \land B & A \times B \\ A \lor B & A + B \\ A \implies B & A \rightarrow B \\ A \iff B & (A \rightarrow B ) \times (B \rightarrow A) \\ \lnot A & A \rightarrow \mathbf{0} \end{array}

証明Aと証明B

$ \frac{x: A \quad y: B }{(x, y) : A \times B}

or(P∨Q)、非交和

$ A + B

If A and Bは関数f : A → Bに対応

A, Bは型

関連

参考

メモ

https://youtu.be/q7zmw8DKx14?si=b433QNewETrOS5Eo